Nuprl Lemma : Rlist-names
11,40
postcript
pdf
Rs
:(Realizer List). R-names(
(
Rs
)) ~ concat(map(
R
.R-names(
R
);
Rs
))
latex
Definitions
Y
,
reduce(
f
;
k
;
as
)
,
map(
f
;
as
)
,
concat(
ll
)
,
(
L
)
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
es
realizer
wf
origin
Rs:(Realizer List). R-names(
(Rs)) ~ concat(map(
R.R-names(R);Rs)) Rs:(Realizer List). R-names((Rs)) ~ concat(map(R.R-names(R);Rs)) (L)
Tx:A. B(x)